Lambda the Ultimate

The correctness of typestate properties in a multithreaded program often depends on the assumption of certain concurrency invariants. However, standard typestate analysis and concurrency analysis are disjoint in that the former is unable to understand threading effects and the latter does not take typestate properties into consideration. We combine these two previously separate approaches and develop a novel typestate-driven concurrency analysis for detecting race conditions and atomicity violations. Our analysis is based on a reformulation of typestate systems in which state transitions of a shared variable are controlled by the locking state of that variable. By combining typestate checking with lockset analysis, we can selectively transfer the typestate to a transient state to simulate the thread interference effect, thus uncovering a new class of typestate errors directly related to low-level or high-level data races. Such a concurrency bug is more likely to be harmful, compared with those found by existing concurrency checkers, because there exists a concrete evidence that it may eventually lead to a typestate error as well. We have implemented a race and atomicity checker for C/C++ programs by extending a NULL pointer dereference analysis. To support large legacy code, our approach does not require a priori annotations; instead, it automatically infers the lock/data guardianship relation and variable correlations. We have applied the toolset to check a future version of the Windows operating system, finding many concurrency errors that cannot be discovered by previous tools.

Typestates extend the ordinary types by recoding the state of objects and allowing the safety violations that stem from operations being invoked on objects that are in the wrong state.

Thought this might be of interest to the Scala (and Twitter and Ruby on Rails) folks here. The Twitter dev team has switched to Scala because RoR couldn't handle the server side traffic. To me this is really interesting since most shops are usually hesitant to switch to "academic" languages, but here we are. And I'm pretty sure its not an April Fool's prank either!

Doron Zeilberger announced yesterday that he has proven that P=NP.

Using 3000 hours of CPU time on a CRAY machine, we settle the notorious P vs. NP problem in the affirmative, by presenting a “polynomial” time algorithm for the NP-complete subset sum problem.

The paper is available here and his 98^th Opinion is offered as commentary.

Due to recent changes in the community which led to less interest in programming language, and the high quality of design discussions unrelated to programming language semantics, the LtU management team has decided to remove the blog portion of the site, and make LtU into a unmoderated forum about all things related to programming, computing, math, and humor.

The blog will migrate temporarily to the url: www.no-such-thing-as-plt.org, to ease the withdrawal pains of regular readers.

This is a good opportunity to thank all the contributing editors for helping the site survive so long by managing to find actual papers about programming language theory, a field that is rumored not to exist.

Urgent update: This message was an April Fools' Day prank.

An historic announcement by Simon Peyton-Jones:

Now that the logo issue finally has been settled, it is time to select the proper Haskell mascot. As you are no doubt aware, Microsoft's involvement in Haskell means that we have moved from avoiding success at all cost to actively marketing the language, and any language striving for success is entirely dependent on a cute and distinctive mascot. Where would Perl be today without its camel?

Since the recent logo discussion has demonstrated once and for all the
futility of attempting a democratic process in the Haskell community -
to be quite honest, the elected logo looks like an error message from an IBM
mainframe - I have decided to decide on a mascot myself.

So I hereby declare the official Haskell mascot to be the koala, in
the form of the image attached below. Please ensure that this image
accompanies any material published on the web or on paper.

The mentioned image can be viewed here.

Gilad Bracha gives a pretty compelling argument with good examples on why we should favor subsumption over other things (ADT/inheritance) in "Subsuming Packages and other Stories".

PLOT: Programming Language for Old Timers by David Moon, 2006-2008.

Programming Language for Old Timers (PLOT) is a new dialect of Lisp designed by Dave Moon in February 2006, and thoroughly revised and simplified November 2007 and March 2008. I have been developing PLOT as a hobby, with the idea of for once having a programming language which does everything the right way. You know it is right when both simplicity and power are maximized, while at the same time confusion and the need for kludges are minimized.

As conferences get older, they tend to require a greater burden of proof. Program committees reject papers as "too early", and want more demonstrations that the ideas are sound. This is why conferences tend to lose the excitement of the early days.

Onward! is a conference that focuses on innovative ideas about software. The program committee is looking for ideas that, if they succeed, will make a big impact. Though the committee has to be convinced that the idea is reasonable, it is less concerned with proof than other program committees. Essays and full papers are due April 20, and short papers are due June 26. Onward! is also looking for workshop proposals and films. See http://www.onward-conference.org/

Essays are an unusual and noteworthy part of Onward! An Onward! essay is a thoughtful reflection about some aspect of sofftware technology. Its goal is to help the reader to share a new insight, engage with an argument, or wrestle with a dilemma.

Some of the essays that have appeared at Onward! are

• Dan Grossman "The transactional memory / garbage collection analogy"
• Dick Gabriel "Designed as Designer"
• Friedrich Steimann "The paradoxical success of aspect-oriented programming"

Although Onward! was originally a part of OOPSLA, and is being colocated with it this year, you can see from these papers that it is not restricted to object-oriented programming, or even programming languages. However, it gives a welcome reception to new ideas in programming languages, so if you have something new that you'd like to promote, I urge you to consider submitting it to Onward!

The Art of the Propagator, Alexey Radul and Gerald Jay Sussman.

We develop a programming model built on the idea that the basic computational elements are autonomous machines interconnected by shared cells through which they communicate. Each machine continuously examines the cells it is interested in, and adds information to some based on deductions it can make from information from the others. This model makes it easy to smoothly combine expression-oriented and constraint-based programming; it also easily accommodates implicit incremental distributed search in ordinary programs. This work builds on the original research of Guy Lewis Steele Jr. and was developed more recently with the help of Chris Hanson.

I just ran across this tech report. I haven't read it yet, but the subject is particularly well-timed for me, since I just finished a correctness proof for a simple FRP system implemented via imperative dataflow graphs, and so constraint propagation has been much on my mind recently. It's pretty clear that constraint propagation can do things that FRP doesn't, but it's not so clear to me whether this is a case of "more expressiveness" or "more fragile abstractions".

The list of accepted papers is out for the IFIP Working Conference on Domain Specific Languages. Happily for me, the program reveals much interest in languages for reasoning, decision making, and search. Even among people who are not my coauthors. :)

Declarative programming tends to attract skepticism because it has the reputation of poor and hard-to-control performance. The approach of DSL embedding appears to ameliorate this problem, and the success of SAT solvers appears to chip away at this reputation.

Meanwhile, the call for papers is out for Principles and Practice of Declarative Programming 2009, which has a venerable program committee. The submission deadline is May 7.